es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }. e(e1,e2].True  (e1 <loc e2) 

latex

Definitions	t  T, x:A. B(x), (e <loc e'), Prop, True, e(e1,e2].P(e), P  Q, P  Q, b, False, A, first(e), , loc(e), Id, P & Q, E, x. t(x), P  Q, ES, A & B, x:A. B(x), e  e'
Lemmas	es-le-self, es-le wf, es-le-trans3, event system wf, existse-between3 wf, true wf, es-E wf, Id wf, es-loc wf, not wf, assert wf, es-first wf, es-loc-pred, es-locl wf